$\forall$${\it the\_es}$:ES, $j$:E. ($\neg$($\uparrow$first($j$))) $\Rightarrow$ pred($j$) $\leq$loc $j$